(set-info :smt-lib-version 2.6)
(set-logic QF_LIA)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)
(declare-fun x5 () Int)
(declare-fun x6 () Int)
(declare-fun x7 () Int)
(declare-fun x8 () Int)
(declare-fun x9 () Int)
(assert (let ((?v_5 (* 0 x1)) (?v_7 (* 1 x2)) (?v_1 (* 1 x4)) (?v_2 (* 1 x6)) (?v_6 (* 0 x7)) (?v_3 (* 0 x8)) (?v_15 (* 0 x2)) (?v_19 (* 1 x8)) (?v_9 (* 0 x3)) (?v_18 (* 1 x9)) (?v_12 (* 0 x0)) (?v_13 (* 0 x9)) (?v_17 (* 1 x5)) (?v_16 (* 1 x0)) (?v_0 (* (- 1) x0)) (?v_4 (* (- 1) x5)) (?v_8 (* (- 1) x2)) (?v_10 (* (- 1) x4)) (?v_14 (* (- 1) x3)) (?v_11 (* (- 1) x6))) (and (<= (+ ?v_0 (+ ?v_5 (+ ?v_7 (+ ?v_1 (+ (* 0 x5) (+ ?v_2 (+ ?v_6 ?v_3))))))) 1) (<= (+ ?v_0 (+ ?v_15 (+ ?v_1 (+ ?v_4 (+ (* 0 x6) ?v_19))))) 0) (<= (+ ?v_8 (+ ?v_9 (+ ?v_2 (+ ?v_3 ?v_18)))) 0) (<= (+ (* (- 2) x2) (+ (* 1 x3) (+ ?v_10 (+ ?v_4 (+ ?v_2 ?v_3))))) (- 1)) (<= (+ ?v_14 (+ ?v_4 (+ ?v_11 (+ ?v_12 (+ ?v_5 (+ ?v_6 (+ ?v_13 ?v_7))))))) 0) (<= (+ ?v_8 (+ ?v_9 (+ ?v_10 (+ ?v_11 (+ (* (- 1) x9) (+ ?v_12 (+ (* 1 x1) ?v_17))))))) 0) (<= (+ (* (- 1) x7) (+ ?v_16 (+ ?v_5 (+ ?v_9 (+ ?v_3 ?v_13))))) (- 1)) (<= (+ ?v_14 (+ ?v_15 (+ ?v_6 (+ ?v_16 (+ ?v_17 ?v_18))))) 1) (<= (+ ?v_11 (+ (* 0 x4) (+ ?v_6 (+ ?v_13 (+ ?v_17 ?v_19))))) 0))))
(check-sat)
(exit)
